English+GermanWikipedia - /page/entry.mu

Micron Document

<!DOCTYPE html>

</head>

</header>

</div>

<p><b>3-SAT</b> ist eine Variante des <a href="Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik" title="Erfüllbarkeitsproblem der Aussagenlogik">Erfüllbarkeitsproblems der Aussagenlogik</a> (von <span style="font-style:normal;font-weight:normal"><a href="Englische_Sprache" title="Englische Sprache">englisch</a></span> <span lang="en-Latn" style="font-style:italic"><i>satisfiability</i></span> ‚Erfüllbarkeit‘, kurz <i>SAT</i>).

</p><p>Es beschäftigt sich mit der Frage, ob eine in <a href="Konjunktive_Normalform" title="Konjunktive Normalform">konjunktiver Normalform</a> vorliegende <a href="Aussagenlogik" title="Aussagenlogik">aussagenlogische</a> <a href="Formel" title="Formel">Formel</a> <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle F}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle F}</annotation>

</semantics>

</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/545fd099af8541605f7ee55f08225526be88ce57.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:1.741ex; height:2.176ex;" alt="{\displaystyle F}" loading="lazy"></span>, die höchstens 3 <a href="Literal" title="Literal">Literale</a> pro <a href="Disjunktionsterm" title="Disjunktionsterm">Klausel</a> enthält, erfüllbar ist.

Ein Beispiel für eine solche Formel:

</p>

<mover>

<msub>

</mrow>

</msub>

</mover>

</mrow>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<mover>

<msub>

</mrow>

</msub>

</mover>

</mrow>

<msub>

</mrow>

</msub>

<msub>

</mrow>

</msub>

<mover>

<msub>

</mrow>

</msub>

</mover>

</mrow>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle F=({\overline {x_{1}}}\vee x_{2}\vee x_{3})\wedge (x_{2}\vee {\overline {x_{3}}}\vee x_{4})\wedge (x_{1}\vee {\overline {x_{2}}})}</annotation>

</semantics>

</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/012b70a30a406e4229e84079b8b0f9ab9d3397cc.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.838ex; width:47.762ex; height:2.843ex;" alt="{\displaystyle F=({\overline {x_{1}}}\vee x_{2}\vee x_{3})\wedge (x_{2}\vee {\overline {x_{3}}}\vee x_{4})\wedge (x_{1}\vee {\overline {x_{2}}})}" loading="lazy"></span></dd></dl>

<p>Gesucht ist nun eine <a href="Belegung_(Mathematik)" title="Belegung (Mathematik)">Belegung</a> der Variablen <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{1}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x_{1}}</annotation>

</semantics>

</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/a8788bf85d532fa88d1fb25eff6ae382a601c308.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{1}}" loading="lazy"></span> bis <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle x_{4}}">

<msub>

</mrow>

</msub>

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle x_{4}}</annotation>

</semantics>

</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/fb828766e82e496666b179ff70d8e2fd24a79e5f.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.671ex; width:2.384ex; height:2.009ex;" alt="{\displaystyle x_{4}}" loading="lazy"></span> mit 0 oder 1, für die F den Wert 1 (wahr) annimmt. Falls es eine solche Belegung gibt, ist F erfüllbar, sonst nicht. Wie bei allen <a href="NP-Vollst%C3%A4ndigkeit" title="NP-Vollständigkeit">NP-vollständigen</a> Problemen ist es „einfach“, einen Lösungskandidaten auf seine Gültigkeit zu überprüfen, hier also festzustellen, ob eine vorgegebene Belegung der Variablen die Formel erfüllt. Das Auffinden eines gültigen Lösungskandidaten ist jedoch im Allgemeinen „schwierig“, da heute keine Methode bekannt ist, eine erfüllende Belegung in polynomieller Zeit zu finden.

</p><p>Allgemeiner definiert man das <i>k-SAT-Problem</i> als die Frage, ob eine beliebige aussagenlogische Formel, die in konjunktiver Normalform mit k Literalen pro Klausel vorliegt, erfüllbar ist. Das k-SAT-Problem für <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle k>3}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle k>3}</annotation>

</semantics>

</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/45c55b4ff0d61c81d264463917a795a521e8e5c8.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:5.472ex; height:2.176ex;" alt="{\displaystyle k>3}" loading="lazy"></span> lässt sich auf 3-SAT zurückführen, damit gilt: Alle k-SAT-Probleme für <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle k\geq 3}">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle k\geq 3}</annotation>

</semantics>

</math></span><img src="./_assets_/eb734a37dd21ce173a46342d1cc64c92/cd0b1582d6f884e01e27786508ef410fae3de5e4.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.505ex; width:5.472ex; height:2.343ex;" alt="{\displaystyle k\geq 3}" loading="lazy"></span> sind NP-vollständig.<sup id="cite_ref-gritzmann2013_1-0" class="reference"><a href="#cite_note-gritzmann2013-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> 2-SAT liegt in der <a href="Komplexit%C3%A4tsklasse" title="Komplexitätsklasse">Komplexitätsklasse</a> <a href="NL_(Komplexit%C3%A4tsklasse)" title="NL (Komplexitätsklasse)">NL</a>, 1-SAT liegt in der Komplexitätsklasse <a href="L_(Komplexit%C3%A4tsklasse)" title="L (Komplexitätsklasse)">L</a>.

</p><p>Das allgemeine <a href="Erf%C3%BCllbarkeitsproblem_der_Aussagenlogik" title="Erfüllbarkeitsproblem der Aussagenlogik">Erfüllbarkeitsproblem der Aussagenlogik</a> (SAT) lässt sich auf 3-SAT <a href="Polynomialzeitreduktion" title="Polynomialzeitreduktion">polynomiell reduzieren</a>, und somit ist 3-SAT nach dem <a href="Satz_von_Cook" title="Satz von Cook">Satz von Cook</a> <a href="NP-Vollst%C3%A4ndigkeit" title="NP-Vollständigkeit">NP-vollständig</a>.

</p><p>3-SAT lässt sich wiederum u. a. auf das <a href="Cliquenproblem" title="Cliquenproblem">Cliquenproblem</a>, das <a href="Rucksackproblem" title="Rucksackproblem">Rucksackproblem</a> und auf den <a href="Hamiltonkreisproblem" title="Hamiltonkreisproblem">gerichteten Hamiltonkreis (DHC)</a> polynomiell <a href="Reduktion_(theoretische_Informatik)" title="Reduktion (theoretische Informatik)">reduzieren</a>, wodurch auch diese Probleme als <a href="NP-Schwere" title="NP-Schwere">NP-schwer</a> nachgewiesen sind.

</p>

<div class="mw-heading mw-heading2"><h2 id="Varianten">Varianten</h2></div>

<div class="mw-heading mw-heading3"><h3 id="Exakt-3-SAT">Exakt-3-SAT</h3></div>

<p>Wenn jede Klausel der Formel genau drei bzw. k Literale enthält, spricht man von Exakt-3-SAT bzw. Exakt-k-SAT.<sup id="cite_ref-gritzmann2013_1-1" class="reference"><a href="#cite_note-gritzmann2013-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> Manchmal wird schon in der Definition von 3-SAT verlangt, dass alle Klauseln genau drei Literale enthalten. Auch diese Variante des Problems ist NP-vollständig, selbst dann, wenn man zusätzlich auch noch verlangt, dass alle Literale in einer Klausel verschieden sind.<sup id="cite_ref-gritzmann2013_1-2" class="reference"><a href="#cite_note-gritzmann2013-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup>

</p>

<p>Hier wird nicht verlangt, dass jede Klausel wahr wird, sondern möglichst viele davon. Bereits eine zufällige Belegung der Variablen liefert im Erwartungswert, dass 7/8 der Klauseln erfüllt sind (denn die Wahrscheinlichkeit, dass eine bestimmte Klausel <i>nicht</i> erfüllt ist, ist lediglich (1/2)^3 – vorausgesetzt, dass Literale nicht mehrfach in einer Klausel auftreten). Die Folge daraus ist auch, dass jedes derartige 3-SAT-Problem mit weniger als 8 Klauseln erfüllbar ist.

</p><p>Max-3-SAT ist ebenfalls NP-vollständig, da die Reduktion zum normalen 3-SAT nur darin besteht zu fragen, ob die Gesamtanzahl der Klauseln erfüllt werden kann.

</p>

<div class="mw-heading mw-heading3"><h3 id="Not-All-Equal-3-SAT">Not-All-Equal-3-SAT</h3></div>

<p>Es handelt sich um 3-SAT, wobei aber nur eine Belegung akzeptiert wird, die in jeder Klausel mindestens ein falsches und ein wahres Literal bewirkt. Not-All-Equal-3-SAT ist ebenfalls NP-vollständig.

</p>

<div class="mw-heading mw-heading2"><h2 id="Literatur">Literatur</h2></div>

<ul><li><a href="Uwe_Sch%C3%B6ning" title="Uwe Schöning">Schöning, Uwe</a>: <a rel="nofollow" class="external text" href="https://www.theorie.physik.uni-goettingen.de/~hartmann/nwgruppe/talks/3sat.ps.gz">Wettlauf um den schnellsten SAT-Algorithmus</a> (<a href="Gzip" title="Gzip">GZIP</a>; 78 kB)</li>

<li><a href="Jon_Kleinberg" title="Jon Kleinberg">Jon Kleinberg</a>, <a href="%C3%89va_Tardos" title="Éva Tardos">Éva Tardos</a>. Algorithm Design. Pearson International Edition, 2006. ISBN 0-321-37291-3. Seiten 724ff (MAX-3-SAT)</li></ul>

<div class="mw-heading mw-heading2"><h2 id="Einzelnachweise">Einzelnachweise</h2></div>

<li id="cite_note-gritzmann2013-1"><span class="mw-cite-backlink">↑ <sup><a href="#cite_ref-gritzmann2013_1-0">a</a></sup> <sup><a href="#cite_ref-gritzmann2013_1-1">b</a></sup> <sup><a href="#cite_ref-gritzmann2013_1-2">c</a></sup></span> <span class="reference-text"><a href="Peter_Gritzmann" title="Peter Gritzmann">Peter Gritzmann</a>: <cite style="font-style:italic">Grundlagen der Mathematischen Optimierung</cite>. Diskrete Strukturen, Komplexitätstheorie, Konvexitätstheorie, Lineare Optimierung, Simplex-Algorithmus, Dualität. Springer, 2013, ISBN 978-3-8348-2011-2, <span style="white-space:nowrap">S.<span style="display:inline-block;width:.2em"> </span>206–208</span>, <a href="Digital_Object_Identifier" title="Digital Object Identifier">doi</a>:<span class="uri-handle" style="white-space:nowrap"><a rel="nofollow" class="external text" href="https://doi.org/10.1007/978-3-8348-2011-2">10.1007/978-3-8348-2011-2</a></span>.<span class="Z3988" title="ctx_ver=Z39.88-2004&rft_val_fmt=info%3Aofi%2Ffmt%3Akev%3Amtx%3Abook&rfr_id=info:sid/de.wikipedia.org:3-SAT&rft.au=Peter+Gritzmann&rft.btitle=Grundlagen+der+Mathematischen+Optimierung&rft.date=2013&rft.doi=10.1007%2F978-3-8348-2011-2&rft.genre=book&rft.isbn=9783834820112&rft.pages=206-208&rft.pub=Springer" style="display:none"> </span></span>

</li>

</ol></div><div><div class="zim-footer">

Dieser Artikel wurde von <a class="external text" title="Zuletzt bearbeitet am 2024-11-16" href="https://de.wikipedia.org/wiki/?title=3-SAT&oldid=250401763">Wikipedia</a> herausgegeben. Der Text ist unter <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.de">Creative Commons Attribution-Share Alike 4.0</a> verfügbar, sofern nicht anders angegeben. Für die Mediendateien können zusätzliche Bedingungen gelten.

</div>

</div></div>

</div>

</main>

</div>

</body></html>